x, y:Atom. x =a y   

latex

ProofTree

Definitions	x =a y, t  T, x:A. B(x), A, P  Q, False
Lemmas	bfalse wf, btrue wf